Nuprl Lemma : qmul_zero_qrng
11,40
postcript
pdf
a
:
. (0 *
a
) = 0
& (
a
* 0) = 0
latex
Definitions
t
T
,
t
.2
,
t
.1
,
CRng
,
<
+*>
,
0
,
*
,
x
f
y
,
|
r
|
,
x
:
A
.
B
(
x
)
Lemmas
crng
wf
,
qrng
wf
,
rng
times
zero
origin
a:
. (0 * a) = 0 
& (a * 0) = 0 a:. (0 * a) = 0 & (a * 0) = 0 T+*>x:A. B(x)